Termination Proof Script

• Consider the SCC {40,55}. There are no usable rules. By taking the AF π with π(CONS) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 40 is weakly decreasing and rule 55 is strictly decreasing. There is one new SCC.
  • Consider the SCC {40}. By taking the AF π with π(CONS) = 1 together with the lexicographic path order with empty precedence, rule 40 is strictly decreasing.


• Consider the SCC {39,54}. There are no usable rules. By taking the AF π with π(FROM) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 39 is weakly decreasing and rule 54 is strictly decreasing. There is one new SCC.
  • Consider the SCC {39}. By taking the AF π with π(FROM) = 1 together with the lexicographic path order with empty precedence, rule 39 is strictly decreasing.


• Consider the SCC {41,56}. There are no usable rules. By taking the AF π with π(mark) = π(S) = 1 together with the lexicographic path order with empty precedence, rule 41 is weakly decreasing and rule 56 is strictly decreasing. There is one new SCC.
  • Consider the SCC {41}. By taking the AF π with π(S) = 1 together with the lexicographic path order with empty precedence, rule 41 is strictly decreasing.


• Consider the SCC {42,43,57}. There are no usable rules. By taking the AF π with π(mark) = π(SEL) = 1 together with the lexicographic path order with empty precedence, the rules in {42,43} are weakly decreasing and rule 57 is strictly decreasing. There is one new SCC.
  • Consider the SCC {42,43}. By taking the AF π with π(SEL) = 1 together with the lexicographic path order with empty precedence, rule 43 is weakly decreasing and rule 42 is strictly decreasing. There is one new SCC.
    • Consider the SCC {43}. By taking the AF π with π(SEL) = 2 together with the lexicographic path order with empty precedence, rule 43 is strictly decreasing.


• Consider the SCC {45,47,48,50,52,53}. There are no usable rules. By taking the AF π with π(from) = π(PROPER) = π(s) = 1 together with the lexicographic path order with empty precedence, the rules in {45,50} are weakly decreasing and the rules in {47,48,52,53} are strictly decreasing. There is one new SCC.
  • Consider the SCC {45,50}. By taking the AF π with π(from) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 45 is weakly decreasing and rule 50 is strictly decreasing. There is one new SCC.
    • Consider the SCC {45}. By taking the AF π with π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 45 is strictly decreasing.


• Consider the SCC {30,32,34,36,38}. There are no usable rules. By taking the AF π with π(ACTIVE) = π(cons) = π(from) = π(s) = 1 together with the lexicographic path order with empty precedence, the rules in {30,32,34} are weakly decreasing and the rules in {36,38} are strictly decreasing. There is one new SCC.
  • Consider the SCC {30,32,34}. By taking the AF π with π(ACTIVE) = π(cons) = π(from) = 1 together with the lexicographic path order with empty precedence, the rules in {30,32} are weakly decreasing and rule 34 is strictly decreasing. There is one new SCC.
    • Consider the SCC {30,32}. By taking the AF π with π(ACTIVE) = π(cons) = 1 together with the lexicographic path order with empty precedence, rule 32 is weakly decreasing and rule 30 is strictly decreasing. There is one new SCC.
      • Consider the SCC {32}. By taking the AF π with π(ACTIVE) = 1 and π(cons) = [1] together with the lexicographic path order with empty precedence, rule 32 is strictly decreasing.


• Consider the SCC {58,60}. The usable rules are {1-22}. The constraints could not be solved.